\begin{tabbing}
es\_realizer\_ind(\=$x_{1}$;\+
\\[0ex]${\it none}$;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.${\it plus}$(${\it left}$;${\it right}$;${\it rec}_{1}$;${\it rec}_{2}$);
\\[0ex]${\it loc}$,$T$,$x$,$v$.${\it init}$(${\it loc}$;$T$;$x$;$v$);
\\[0ex]${\it loc}$,$T$,$x$,$L$.${\it frame}$(${\it loc}$;$T$;$x$;$L$);
\\[0ex]${\it lnk}$,${\it tag}$,$L$.${\it sframe}$(${\it lnk}$;${\it tag}$;$L$);
\\[0ex]${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$.${\it effect}$(${\it loc}$;${\it ds}$;${\it knd}$;$T$;$x$;$f$);
\\[0ex]${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$.${\it sends}$(${\it ds}$;${\it knd}$;$T$;$l$;${\it dt}$;$g$);
\\[0ex]${\it loc}$,${\it ds}$,$a$,$p$,$P$.${\it pre}$(${\it loc}$;${\it ds}$;$a$;$p$;$P$);
\\[0ex]${\it loc}$,$k$,$L$.${\it aframe}$(${\it loc}$;$k$;$L$);
\\[0ex]${\it loc}$,$k$,$L$.${\it bframe}$(${\it loc}$;$k$;$L$);
\\[0ex]${\it loc}$,$x$,$L$.${\it rframe}$(${\it loc}$;$x$;$L$))
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $x_{1}$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it none}$\+
\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it plus}$\=($x$.1\+\+
\\[0ex];$x$.2
\\[0ex];es\_realizer\_ind(\=($x$.1);\+
\\[0ex]${\it none}$;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.${\it plus}$\=(${\it left}$\+
\\[0ex];${\it right}$
\\[0ex];${\it rec}_{1}$
\\[0ex];${\it rec}_{2}$);
\-\\[0ex]${\it loc}$,$T$,$x$,$v$.${\it init}$(${\it loc}$;$T$;$x$;$v$);
\\[0ex]${\it loc}$,$T$,$x$,$L$.${\it frame}$(${\it loc}$;$T$;$x$;$L$);
\\[0ex]${\it lnk}$,${\it tag}$,$L$.${\it sframe}$(${\it lnk}$;${\it tag}$;$L$);
\\[0ex]${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$.${\it effect}$\=(${\it loc}$\+
\\[0ex];${\it ds}$
\\[0ex];${\it knd}$
\\[0ex];$T$
\\[0ex];$x$
\\[0ex];$f$);
\-\\[0ex]${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$.${\it sends}$\=(${\it ds}$\+
\\[0ex];${\it knd}$
\\[0ex];$T$
\\[0ex];$l$
\\[0ex];${\it dt}$
\\[0ex];$g$);
\-\\[0ex]${\it loc}$,${\it ds}$,$a$,$p$,$P$.${\it pre}$(${\it loc}$;${\it ds}$;$a$;$p$;$P$);
\\[0ex]${\it loc}$,$k$,$L$.${\it aframe}$(${\it loc}$;$k$;$L$);
\\[0ex]${\it loc}$,$k$,$L$.${\it bframe}$(${\it loc}$;$k$;$L$);
\\[0ex]${\it loc}$,$x$,$L$.${\it rframe}$(${\it loc}$;$x$;$L$))
\-\\[0ex];es\_realizer\_ind(\=($x$.2);\+
\\[0ex]${\it none}$;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.${\it plus}$\=(${\it left}$\+
\\[0ex];${\it right}$
\\[0ex];${\it rec}_{1}$
\\[0ex];${\it rec}_{2}$);
\-\\[0ex]${\it loc}$,$T$,$x$,$v$.${\it init}$(${\it loc}$;$T$;$x$;$v$);
\\[0ex]${\it loc}$,$T$,$x$,$L$.${\it frame}$(${\it loc}$;$T$;$x$;$L$);
\\[0ex]${\it lnk}$,${\it tag}$,$L$.${\it sframe}$(${\it lnk}$;${\it tag}$;$L$);
\\[0ex]${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$.${\it effect}$\=(${\it loc}$\+
\\[0ex];${\it ds}$
\\[0ex];${\it knd}$
\\[0ex];$T$
\\[0ex];$x$
\\[0ex];$f$);
\-\\[0ex]${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$.${\it sends}$\=(${\it ds}$\+
\\[0ex];${\it knd}$
\\[0ex];$T$
\\[0ex];$l$
\\[0ex];${\it dt}$
\\[0ex];$g$);
\-\\[0ex]${\it loc}$,${\it ds}$,$a$,$p$,$P$.${\it pre}$(${\it loc}$;${\it ds}$;$a$;$p$;$P$);
\\[0ex]${\it loc}$,$k$,$L$.${\it aframe}$(${\it loc}$;$k$;$L$);
\\[0ex]${\it loc}$,$k$,$L$.${\it bframe}$(${\it loc}$;$k$;$L$);
\\[0ex]${\it loc}$,$x$,$L$.${\it rframe}$(${\it loc}$;$x$;$L$)))
\-\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it init}$($x$.1;($x$.2).1;($x$.2.2).1;$x$.2.2.2)\+
\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it frame}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];($x$.2.2).1
\\[0ex];$x$.2.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it sframe}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];$x$.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it effect}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];($x$.2.2).1
\\[0ex];($x$.2.2.2).1
\\[0ex];($x$.2.2.2.2).1
\\[0ex];$x$.2.2.2.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it sends}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];($x$.2.2).1
\\[0ex];($x$.2.2.2).1
\\[0ex];($x$.2.2.2.2).1
\\[0ex];$x$.2.2.2.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it pre}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];($x$.2.2).1
\\[0ex];($x$.2.2.2).1
\\[0ex];$x$.2.2.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it aframe}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];$x$.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ \=case $x$\+
\\[0ex]o\=f inl($x$) =$>$ ${\it bframe}$\=($x$.1\+\+
\\[0ex];($x$.2).1
\\[0ex];$x$.2.2)
\-\\[0ex]$\mid$ inr($x$) =$>$ ${\it rframe}$\=($x$.1\+
\\[0ex];($x$.2).1
\\[0ex];$x$.2.2)
\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\-\\[0ex]\emph{(recursive)}
\end{tabbing}